#SMT, or model counting for logical theories, is a well-known hard problemthat generalizes such tasks as counting the number of satisfying assignments toa Boolean formula and computing the volume of a polytope. In the realm ofsatisfiability modulo theories (SMT) there is a growing need for model countingsolvers, coming from several application domains (quantitative informationflow, static analysis of probabilistic programs). In this paper, we show areduction from an approximate version of #SMT to SMT. We focus on the theories of integer arithmetic and linear real arithmetic. Wepropose model counting algorithms that provide approximate solutions withformal bounds on the approximation error. They run in polynomial time and makea polynomial number of queries to the SMT solver for the underlying theory,exploiting "for free" the sophisticated heuristics implemented within modernSMT solvers. We have implemented the algorithms and used them to solve thevalue problem for a model of loop-free probabilistic programs withnondeterminism.
展开▼
